\section{Policy}\label{sec:policy}
All aspects of a system using the Muen kernel must be specified in a policy XML
file. The policy is composed of the following main parts:

\begin{itemize}
	\item Hardware
	\item Kernel
	\item Binaries
	\item Subjects
	\item Scheduling
\end{itemize}

XML was chosen as a specification language since it is human-readable and can
be automatically verified against a schema. Furthermore, there is an existing
Ada library called XML/Ada \cite{xmlada}, which is open source.

The policy contained in the XML file is transformed into SPARK source by the
policy compilation tool \texttt{skpolicy}. The process is described in detail in
section \ref{subsec:policy-compilation}.

Each of the main policy parts are presented in the following sections. Preceding
these descriptions is the specification of data types, which are the basis for
the subsequent definition of policy elements. The data types and elements map
directly to their corresponding XML schema definitions.

The type constraints are enforced during policy compilation by means of schema
validation. Additional checks are implemented manually in the policy compiler.

\subsection{Data Types}
This section describes basic data types that are used in the specification of
the system policy. They are referenced in later chapters as part of the
definition of other XML schema elements.

\input{types.tex}

\subsection{Hardware}\label{subsec:hardware}
\input{hardware.tex}

\subsection{Kernel}
\input{kernel.tex}

\subsection{Binaries}
\input{binary.tex}

\clearpage
\subsection{Subjects}\label{subsec:subjects}
\input{subject.tex}

\subsection{Scheduling}
\input{scheduling.tex}
